#ifndef ARRINT_H
#define ARRINT_H

typedef struct sArrInt *arrInt;

/* Nota: a=A => created(a) */

/* Constructores y destructor */

arrInt
arrInt_create(const int ne);
/*
  DESC: Constructor del tipo
  PRE: { ne >= 0 /\ ! created(a) }
  a = arrInt_create(ne);
  POS: { Hay memoria ==> a = A /\ length(a)=ne }
*/

arrInt
arrInt_clone(const arrInt a);
/*
  DESC: Construye una copia.
  PRE: { a=A /\ ! created(b) }
  b = arrInt_clone(a);
  POS: { Hay memoria ==> a=A /\ b=a }
*/

void
arrInt_destroy(arrInt a);
/*
  DESC: Destructor de tipo. Cambia a.
  PRE: { a=A }
  arrInt_destroy(a);
  POS: { ! created(a) }
*/

/* Proyector */

int
arrInt_length(const arrInt a);
/*
  DESC: Devuelve el tamanio.
  PRE: { a=A }
  l = arrInt_length(a);
  POS: { a=A /\ l=length(a) }
*/

/* Procedimientos */

void
arrInt_swap(arrInt a, const int i, const int j);
/*
  DESC: Hace el swap entre las posiciones i y j. Cambia a.
  PRE: { a=A /\ 0 <= i,j < length(a) }
  arrInt_swap(a,i,j);
  POS: { a=swap(A,i,j) }
*/

void
arrInt_reverse(arrInt a);
/*
  DESC: Hace el reverse de a. Cambia a.
  PRE: { a=A }
  arrInt_reverse(a);
  POS: { (FORALL i: 0<= i < length(a): a[i] = A[length(A)-i-1]) /\ length(a)=length(A) }
*/

void
arrInt_fillStdIn(arrInt a);
/*
  DESC: Llena a por teclado. Cambia a.
  PRE: { a=A }
  arrInt_fillStdIn(a);
  POS: { llenado a por teclado /\ length(a)=length(A) }
*/

void
arrInt_fillRand(arrInt a);
/*
  DESC: Llena a con valores al azar. Cambia a.
  PRE: { a=A }
  arrInt_fillRand(a);
  POS: { llenado a con valores al azar /\ length(a)=length(A) }
*/

void
arrInt_showStdOut(const arrInt a);
/*
  DESC: Muestra por pantalla los valores en a.
  PRE: { a=A }
  arrInt_showStdOut(a);
  POS: { a=A /\ Valores de A en pantalla }
*/

void
arrInt_copy(arrInt b, const arrInt a);
/*
  DESC: Copia el objeto a en b.
  PRE: { a=A /\ b=B /\ length(a) <= length(b)}
  arrInt_copy(b,a);
  POS: { a=A /\ b=a }
*/

#endif /* ARRINT_H */

